\begin{tabbing}
sends1{-}p(${\it es}$;$x$;$A$;$k$;$B$;$l$;${\it tg}$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=((vartype(source($l$);$x$) $\subseteq$r $A$)\+
\\[0ex]\& ($\forall$$e$:E. (loc($e$) = source($l$)) $\Rightarrow$ (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r $B$))
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$)))
\\[0ex]c$\wedge$ \=($\forall$$e$:E.\+
\\[0ex](loc($e$) = source($l$))
\\[0ex]$\Rightarrow$ (kind($e$) = $k$)
\\[0ex]$\Rightarrow$ ($\exists$\=$L$:\{${\it e'}$:E$\mid$ kind(${\it e'}$) = rcv($l$,${\it tg}$)\}  List\+
\\[0ex](($\forall$${\it e'}$:E. (${\it e'}$ $\in$ $L$) $\Leftarrow\!\Rightarrow$ ((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (sender(${\it e'}$) = $e$)))
\\[0ex]\& ($\forall$$e_{1}$, $e_{2}$:E. $e_{1}$ before $e_{2}$ $\in$ $L$ $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\\[0ex]\& map($\lambda$${\it e'}$.val(${\it e'}$);$L$) = $f$(($x$ when $e$),val($e$)))))
\-\-\-
\end{tabbing}